es:ES, l:IdLnk, tgs:Id List, da:k:Knd fp Type, f1,
f2:({e:E| loc(e) = source(l)  Id }((tg:Idda(rcv(l,tg))?Void) List)), ds1, ds2:x:Id fp Type.
ds2  ds1
 (e:{e:E| loc(e) = source(l)  Id }. f1(e) = f2(e))
 with decls ds1 dasends on l from e include f1(e) and only these for tags in tgs
 with decls ds2 dasends on l from e include f2(e) and only these for tags in tgs 

latex

Definitions

x:A. B(x), P  Q, x(s), with decls ds dasends on l from e include f(e) and only these for tags in tgs, A & B, P & Q, t  T, Prop, x. t(x), f(x)?z, Top, if b t else f fi, true, false, e@i. P(e), SQType(T), {T}, T, True, P  Q, P  Q, Dec(P), P  Q, Id, A, , Unit, False, {i..j},

Lemmas

es-sends-iff wf, es-E wf, Id wf, es-loc wf, lsrc wf, assert wf, es-isrcv wf, IdLnk wf, es-lnk wf, l member wf, es-tag wf, es-valtype wf, fpf-cap wf, Knd wf, Kind-deq wf, es-kind wf, es-vartype wf, id-deq wf, top wf, rcv wf, fpf-sub wf, fpf wf, event system wf, subtype rel transitivity, subtype rel self, decidable assert, fpf-dom wf, fpf-trivial-subtype-top, fpf-cap functionality wrt sub, bool wf, eqtt to assert, iff transitivity, bnot wf, not wf, eqff to assert, assert of bnot, deq wf, length wf1, squash wf, true wf, es-loc-sender, ldst wf, es-index wf, int seg wf, es-Msgl wf, es-sends wf, es-sender wf, select wf, le wf, non neg length